Nuprl Lemma : chain-order-antisymmetric 13,45

es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), SysOut:AbsInterface(Top).
(E(Inr E(Sys))
 (f:sys-antecedent(es;Sys), chain:(E(Sys)(Id List)).
 chain-consistent(f;chain (xy:Id. x << y  (y << x))) 
latex


Upabstract chain replication
Definitionsx << y, #$n, ||as||, (x  l), Atom$n, no_repeats(T;l), adjacent(T;L;x;y), L1  L2, hd(l), a < b, P  Q, e c e', {x:AB(x)} , e  X, E, P & Q, xt(x), x.A(x), pred(e), <ab>, first(e), suptype(ST), S  T, Top, x:A.B(x), x,yt(x;y), pred!(e;e'), SWellFounded(R(x;y)), constant_function(f;A;B), b, , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , type List, Msg(M), kind(e), loc(e), Knd, kindcase(ka.f(a); l,t.g(l;t) ), EOrderAxioms(Epred?info), IdLnk, left + right, Unit, EqDecider(T), , a:A fp B(a), EState(T), A, !Void(), P  Q, strong-subtype(A;B), False, chain-consistent(f;chain), sys-antecedent(es;Sys), AbsInterface(A), Type, ES, x:AB(x), E(X), , x:A  B(x), x before y  l, Id, x:AB(x), x:AB(x), s = t, f(a), t  T, , {T}, increasing(f;k)
Lemmasl before antisymmetry, l before sublist, l before wf, Id wf, es-E-interface wf, false wf, not wf, event system wf, subtype rel wf, EState wf, rationals wf, member wf, strongwellfounded wf, pred! wf, unit wf, top wf, first wf, assert wf, loc wf, constant function wf, IdLnk wf, kindcase wf, Knd wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, kind wf, EOrderAxioms wf, deq wf, es-E wf, es-is-interface wf, es-interface wf, sys-antecedent wf, es-causle wf, chain-consistent wf

origin